; EXPECT: unsat
(set-logic ALL)
(declare-const _vp1-1 (_ BitVec 1))
(declare-const _vp1-2 (_ BitVec 1))
(declare-const _vp1-3 (_ BitVec 1))
(declare-const x796__fresh Bool)
(declare-const x836__fresh Bool)
(declare-const x322__fresh Bool)
(define-fun bit-1 ((bv (_ BitVec 4))) (_ BitVec 4) (bvand bv (bvneg bv)))
(define-fun bit-2 ((bv (_ BitVec 4))) (_ BitVec 4) (bit-1 (bvand bv (bvsub bv (_ bv1 4)))))
(define-fun index-bit ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 4) (ite x836__fresh (bit-1 bv) (bit-2 bv)))
(define-fun permute ((index (_ BitVec 4)) (obj-0 (_ BitVec 4)) (obj-1 (_ BitVec 4)) (obj-2 (_ BitVec 4)) (obj-3 (_ BitVec 4))) (_ BitVec 4) (ite x836__fresh (_ bv0 4) (_ bv0 4)))
(define-fun left-zeros ((index (_ BitVec 4))) (_ BitVec 8) (ite false (_ bv0 8) (_ bv0 8)))
(define-fun centered ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 8) (bvshl ((_ zero_extend 4) bv) (left-zeros index)))
(assert (= (_ bv0 8) (bvxor (_ bv1 8) (bvand (centered (index-bit (_ bv0 4) ((_ zero_extend 3) _vp1-3)) ((_ zero_extend 3) _vp1-3)) (centered ((_ zero_extend 3) _vp1-3) (index-bit ((_ zero_extend 3) _vp1-3) (permute (_ bv1 4) (_ bv0 4) (_ bv0 4) (_ bv0 4) (_ bv0 4))))))))
(check-sat)
